Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(f(a)) → f(g(f(a)))

The replacement map contains the following entries:

f: empty set
a: empty set
g: {1}


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(f(a)) → f(g(f(a)))

The replacement map contains the following entries:

f: empty set
a: empty set
g: {1}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(f(a)) → f(g(f(a)))

The replacement map contains the following entries:

f: empty set
a: empty set
g: {1}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {g} are replacing on all positions.
The symbols in {f, F, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(f(a)) → F(g(f(a)))


The hidden terms of R are:

f(a)

Every hiding context is built from:

g on positions {1}

Hence, the new unhiding pairs DPu are :

U(g(x_0)) → U(x_0)
U(f(a)) → F(a)

The TRS R consists of the following rules:

f(f(a)) → f(g(f(a)))

The set Q consists of the following terms:

f(f(a))


The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 1 less node.
The rules F(f(a)) → F(g(f(a))) and F(f(a)) → F(g(f(a))) form no chain, because ECapµ(F(g(f(a)))) = F(g(f(a))) does not unify with F(f(a)). The rules U(f(a)) → F(a) and F(f(a)) → F(g(f(a))) form no chain, because ECapµ(F(a)) = F(a) does not unify with F(f(a)). 

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {g} are replacing on all positions.
The symbols in {f, U} are not replacing on any position.

The TRS P consists of the following rules:

U(g(x_0)) → U(x_0)

The TRS R consists of the following rules:

f(f(a)) → f(g(f(a)))

The set Q consists of the following terms:

f(f(a))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(g(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof
                ↳ QCSDP
                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {g} are replacing on all positions.
The symbols in {f} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

f(f(a)) → f(g(f(a)))

The set Q consists of the following terms:

f(f(a))


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.